the_w:World, e, e':E. e = e'  e = e' 

latex

Definitions	AB, p = q, E, p  q, a = b, i=j, isnull(a), 1of(t), a(i;t), x. t(x), World, P  Q, P  Q, t  T, Prop, x:A. B(x), P & Q, A, b, , Id, 2of(t)
Lemmas	assert wf, assert of eq int, assert-eq-id, and functionality wrt iff, assert of band, iff transitivity, world wf, pi2 wf, w-a wf, pi1 wf, w-isnull wf, not wf, nat wf, Id wf, eq int wf, eq id wf, band wf, le wf